$\forall$$i$:Id, $T$:Type, $v$:$T$, $x$:Id.
\\[0ex]@$i$: $x$:$T$ initially $x$ = $v$ realizes ${\it es}$. vartype($i$;$x$) $\subseteq\rho$ $T$ \& $x$ initially@$i$  $=$ $v$